YES 15.915000000000001
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule List
| ((elemIndex :: Float -> [Float] -> Maybe Int) :: Float -> [Float] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (\vv1 ->
case | vv1 of |
| (x,i) | -> | if p x then i : [] else [] |
| _ | -> | [] |
) (zip xs (enumFrom 0)) |
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : _) | = | Just a |
|
Lambda Reductions:
The following Lambda expression
\vv1→
case | vv1 of |
| (x,i) | → if p x then i : [] else [] |
| _ | → [] |
is transformed to
findIndices0 | p vv1 | =
case | vv1 of | | (x,i) | → if p x then i : [] else [] |
| _ | → [] |
|
The following Lambda expression
\ab→(a,b)
is transformed to
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
mainModule List
| ((elemIndex :: Float -> [Float] -> Maybe Int) :: Float -> [Float] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = |
case | vv1 of |
| (x,i) | -> | if p x then i : [] else [] |
| _ | -> | [] |
|
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : _) | = | Just a |
|
Case Reductions:
The following Case expression
case | vv1 of |
| (x,i) | → if p x then i : [] else [] |
| _ | → [] |
is transformed to
findIndices00 | p (x,i) | = if p x then i : [] else [] |
findIndices00 | p _ | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
mainModule List
| ((elemIndex :: Float -> [Float] -> Maybe Int) :: Float -> [Float] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | if p x then i : [] else [] |
findIndices00 | p _ | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : _) | = | Just a |
|
If Reductions:
The following If expression
if p x then i : [] else []
is transformed to
findIndices000 | i True | = i : [] |
findIndices000 | i False | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule List
| ((elemIndex :: Float -> [Float] -> Maybe Int) :: Float -> [Float] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p _ | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : _) | = | Just a |
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((elemIndex :: Float -> [Float] -> Maybe Int) :: Float -> [Float] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : vx) | = | Just a |
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
mainModule List
| ((elemIndex :: Float -> [Float] -> Maybe Int) :: Float -> [Float] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : vx) | = | Just a |
|
Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule List
| (elemIndex :: Float -> [Float] -> Maybe Int) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndex :: Eq a => a -> [a] -> Maybe Int
elemIndex | x | = | findIndex (== x) |
|
| findIndex :: (a -> Bool) -> [a] -> Maybe Int
findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero))) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
| listToMaybe :: [a] -> Maybe a
listToMaybe | [] | = | Nothing |
listToMaybe | (a : vx) | = | Just a |
|
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(wz5300), Succ(wz400000)) → new_primPlusNat(wz5300, wz400000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(wz5300), Succ(wz400000)) → new_primPlusNat(wz5300, wz400000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(wz3100), Succ(wz40100)) → new_primMulNat(wz3100, Succ(wz40100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(wz3100), Succ(wz40100)) → new_primMulNat(wz3100, Succ(wz40100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs(wz123, Succ(wz18000), Succ(wz22500), wz224) → new_psPs(wz123, wz18000, wz22500, wz224)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs(wz123, Succ(wz18000), Succ(wz22500), wz224) → new_psPs(wz123, wz18000, wz22500, wz224)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs1(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs1(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs1(wz125, Succ(wz1820), wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_foldr(wz310, :(wz4110, wz4111), wz125) → new_foldr0(wz310, wz4110, wz4111, new_primPlusNat0(wz125, Succ(Zero)), new_primPlusNat0(wz125, Succ(Zero)))
new_foldr0(wz310, Float(Pos(wz41000), wz4101), wz411, wz126, wz125) → new_psPs0(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr0(wz310, Float(Neg(wz41000), wz4101), wz411, wz126, wz125) → new_psPs1(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_psPs1(wz125, Succ(wz1820), wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Succ(wz1810), wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Succ(wz1810), wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs1(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs1(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_foldr(wz310, :(wz4110, wz4111), wz125) → new_foldr0(wz310, wz4110, wz4111, new_primPlusNat0(wz125, Succ(Zero)), new_primPlusNat0(wz125, Succ(Zero)))
new_foldr0(wz310, Float(Pos(wz41000), wz4101), wz411, wz126, wz125) → new_psPs0(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr0(wz310, Float(Neg(wz41000), wz4101), wz411, wz126, wz125) → new_psPs1(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs1(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs1(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_foldr(wz310, :(wz4110, wz4111), wz125) → new_foldr0(wz310, wz4110, wz4111, new_primPlusNat0(wz125, Succ(Zero)), new_primPlusNat0(wz125, Succ(Zero)))
new_foldr0(wz310, Float(Pos(wz41000), wz4101), wz411, wz126, wz125) → new_psPs0(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr0(wz310, Float(Neg(wz41000), wz4101), wz411, wz126, wz125) → new_psPs1(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs1(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs1(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_psPs0(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
new_foldr(wz310, :(wz4110, wz4111), wz125) → new_foldr0(wz310, wz4110, wz4111, new_primPlusNat0(wz125, Succ(Zero)), new_primPlusNat0(wz125, Succ(Zero)))
new_foldr0(wz310, Float(Neg(wz41000), wz4101), wz411, wz126, wz125) → new_psPs1(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr0(wz310, Float(Pos(wz41000), wz4101), wz411, wz126, wz125) → new_psPs0(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr(wz310, :(wz4110, wz4111), wz125) → new_foldr0(wz310, wz4110, wz4111, new_primPlusNat0(wz125, Succ(Zero)), new_primPlusNat0(wz125, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
- new_foldr0(wz310, Float(Neg(wz41000), wz4101), wz411, wz126, wz125) → new_psPs1(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
The graph contains the following edges 5 >= 1, 1 >= 3, 2 > 4, 3 >= 5
- new_foldr0(wz310, Float(Pos(wz41000), wz4101), wz411, wz126, wz125) → new_psPs0(wz125, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
The graph contains the following edges 5 >= 1, 1 >= 3, 2 > 4, 3 >= 5
- new_psPs0(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
- new_psPs0(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
- new_psPs1(wz125, Zero, wz310, Neg(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
- new_psPs1(wz125, Zero, wz310, Pos(wz41010), wz411) → new_foldr(wz310, wz411, wz125)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs2(wz143, Succ(wz1850), wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs3(wz143, Zero, wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_foldr1(wz45, wz430, :(wz4610, wz4611), wz143) → new_foldr2(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz143, Succ(Zero)), new_primPlusNat0(wz143, Succ(Zero)))
new_psPs3(wz143, Succ(wz1860), wz430, Pos(wz46010), wz45, :(wz4610, wz4611)) → new_foldr2(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz143, Succ(Zero)), new_primPlusNat0(wz143, Succ(Zero)))
new_foldr2(wz45, wz430, Float(Neg(wz46000), wz4601), wz461, wz144, wz143) → new_psPs3(wz143, new_primMulNat0(Succ(wz45), wz46000), wz430, wz4601, wz45, wz461)
new_psPs2(wz143, Succ(wz1850), wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_foldr2(wz45, wz430, Float(Pos(wz46000), wz4601), wz461, wz144, wz143) → new_psPs2(wz143, new_primMulNat0(Succ(wz45), wz46000), wz430, wz4601, wz45, wz461)
new_psPs3(wz143, Succ(wz1860), wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs2(wz143, Zero, wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs2(wz143, Zero, wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs3(wz143, Zero, wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs2(wz143, Succ(wz1850), wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs3(wz143, Zero, wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_foldr1(wz45, wz430, :(wz4610, wz4611), wz143) → new_foldr2(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz143, Succ(Zero)), new_primPlusNat0(wz143, Succ(Zero)))
new_psPs3(wz143, Succ(wz1860), wz430, Pos(wz46010), wz45, :(wz4610, wz4611)) → new_foldr2(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz143, Succ(Zero)), new_primPlusNat0(wz143, Succ(Zero)))
new_foldr2(wz45, wz430, Float(Neg(wz46000), wz4601), wz461, wz144, wz143) → new_psPs3(wz143, new_primMulNat0(Succ(wz45), wz46000), wz430, wz4601, wz45, wz461)
new_psPs2(wz143, Succ(wz1850), wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_foldr2(wz45, wz430, Float(Pos(wz46000), wz4601), wz461, wz144, wz143) → new_psPs2(wz143, new_primMulNat0(Succ(wz45), wz46000), wz430, wz4601, wz45, wz461)
new_psPs3(wz143, Succ(wz1860), wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs2(wz143, Zero, wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs2(wz143, Zero, wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
new_psPs3(wz143, Zero, wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
The TRS R consists of the following rules:
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr1(wz45, wz430, :(wz4610, wz4611), wz143) → new_foldr2(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz143, Succ(Zero)), new_primPlusNat0(wz143, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4
- new_foldr2(wz45, wz430, Float(Pos(wz46000), wz4601), wz461, wz144, wz143) → new_psPs2(wz143, new_primMulNat0(Succ(wz45), wz46000), wz430, wz4601, wz45, wz461)
The graph contains the following edges 6 >= 1, 2 >= 3, 3 > 4, 1 >= 5, 4 >= 6
- new_foldr2(wz45, wz430, Float(Neg(wz46000), wz4601), wz461, wz144, wz143) → new_psPs3(wz143, new_primMulNat0(Succ(wz45), wz46000), wz430, wz4601, wz45, wz461)
The graph contains the following edges 6 >= 1, 2 >= 3, 3 > 4, 1 >= 5, 4 >= 6
- new_psPs3(wz143, Succ(wz1860), wz430, Pos(wz46010), wz45, :(wz4610, wz4611)) → new_foldr2(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz143, Succ(Zero)), new_primPlusNat0(wz143, Succ(Zero)))
The graph contains the following edges 5 >= 1, 3 >= 2, 6 > 3, 6 > 4
- new_psPs3(wz143, Zero, wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs3(wz143, Succ(wz1860), wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs3(wz143, Zero, wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs2(wz143, Succ(wz1850), wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs2(wz143, Succ(wz1850), wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs2(wz143, Zero, wz430, Neg(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs2(wz143, Zero, wz430, Pos(wz46010), wz45, wz461) → new_foldr1(wz45, wz430, wz461, wz143)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs5(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs4(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs5(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr4(wz310, Float(Pos(wz41000), wz4101), wz411, wz122, wz121) → new_psPs4(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_psPs4(wz121, Succ(wz1770), wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs5(wz121, Succ(wz1780), wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr4(wz310, Float(Neg(wz41000), wz4101), wz411, wz122, wz121) → new_psPs5(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr3(wz310, :(wz4110, wz4111), wz121) → new_foldr4(wz310, wz4110, wz4111, new_primPlusNat0(wz121, Succ(Zero)), new_primPlusNat0(wz121, Succ(Zero)))
new_psPs4(wz121, Succ(wz1770), wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs4(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs5(wz121, Succ(wz1780), wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs5(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs5(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs4(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr4(wz310, Float(Pos(wz41000), wz4101), wz411, wz122, wz121) → new_psPs4(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr4(wz310, Float(Neg(wz41000), wz4101), wz411, wz122, wz121) → new_psPs5(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_psPs4(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr3(wz310, :(wz4110, wz4111), wz121) → new_foldr4(wz310, wz4110, wz4111, new_primPlusNat0(wz121, Succ(Zero)), new_primPlusNat0(wz121, Succ(Zero)))
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs5(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs5(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs4(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr4(wz310, Float(Pos(wz41000), wz4101), wz411, wz122, wz121) → new_psPs4(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr4(wz310, Float(Neg(wz41000), wz4101), wz411, wz122, wz121) → new_psPs5(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_psPs4(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr3(wz310, :(wz4110, wz4111), wz121) → new_foldr4(wz310, wz4110, wz4111, new_primPlusNat0(wz121, Succ(Zero)), new_primPlusNat0(wz121, Succ(Zero)))
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs5(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs4(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_psPs5(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
new_foldr4(wz310, Float(Pos(wz41000), wz4101), wz411, wz122, wz121) → new_psPs4(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr4(wz310, Float(Neg(wz41000), wz4101), wz411, wz122, wz121) → new_psPs5(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
new_foldr3(wz310, :(wz4110, wz4111), wz121) → new_foldr4(wz310, wz4110, wz4111, new_primPlusNat0(wz121, Succ(Zero)), new_primPlusNat0(wz121, Succ(Zero)))
new_psPs4(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr3(wz310, :(wz4110, wz4111), wz121) → new_foldr4(wz310, wz4110, wz4111, new_primPlusNat0(wz121, Succ(Zero)), new_primPlusNat0(wz121, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
- new_foldr4(wz310, Float(Neg(wz41000), wz4101), wz411, wz122, wz121) → new_psPs5(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
The graph contains the following edges 5 >= 1, 1 >= 3, 2 > 4, 3 >= 5
- new_foldr4(wz310, Float(Pos(wz41000), wz4101), wz411, wz122, wz121) → new_psPs4(wz121, new_primMulNat0(Zero, wz41000), wz310, wz4101, wz411)
The graph contains the following edges 5 >= 1, 1 >= 3, 2 > 4, 3 >= 5
- new_psPs4(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
- new_psPs4(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
- new_psPs5(wz121, Zero, wz310, Neg(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
- new_psPs5(wz121, Zero, wz310, Pos(wz41010), wz411) → new_foldr3(wz310, wz411, wz121)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldr6(wz310, wz4110, wz4111, wz223, wz222) → new_foldr5(wz310, wz4111, wz222)
new_foldr5(wz310, :(wz4110, wz4111), wz127) → new_foldr6(wz310, wz4110, wz4111, new_primPlusNat0(wz127, Succ(Zero)), new_primPlusNat0(wz127, Succ(Zero)))
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
The set Q consists of the following terms:
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr5(wz310, :(wz4110, wz4111), wz127) → new_foldr6(wz310, wz4110, wz4111, new_primPlusNat0(wz127, Succ(Zero)), new_primPlusNat0(wz127, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
- new_foldr6(wz310, wz4110, wz4111, wz223, wz222) → new_foldr5(wz310, wz4111, wz222)
The graph contains the following edges 1 >= 1, 3 >= 2, 5 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldr8(wz45, wz430, Float(Pos(wz46000), wz4601), :(wz4610, wz4611), wz146, wz145) → new_foldr8(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz145, Succ(Zero)), new_primPlusNat0(wz145, Succ(Zero)))
new_foldr8(wz45, wz430, Float(Neg(wz46000), wz4601), wz461, wz146, wz145) → new_foldr7(wz45, wz430, wz461, wz145)
new_foldr7(wz45, wz430, :(wz4610, wz4611), wz145) → new_foldr8(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz145, Succ(Zero)), new_primPlusNat0(wz145, Succ(Zero)))
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
The set Q consists of the following terms:
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr8(wz45, wz430, Float(Pos(wz46000), wz4601), :(wz4610, wz4611), wz146, wz145) → new_foldr8(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz145, Succ(Zero)), new_primPlusNat0(wz145, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4
- new_foldr8(wz45, wz430, Float(Neg(wz46000), wz4601), wz461, wz146, wz145) → new_foldr7(wz45, wz430, wz461, wz145)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 6 >= 4
- new_foldr7(wz45, wz430, :(wz4610, wz4611), wz145) → new_foldr8(wz45, wz430, wz4610, wz4611, new_primPlusNat0(wz145, Succ(Zero)), new_primPlusNat0(wz145, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldr10(wz310, Float(Neg(wz41000), wz4101), wz411, wz124, wz123) → new_foldr9(wz310, wz411, wz123)
new_foldr9(wz310, :(wz4110, wz4111), wz123) → new_foldr10(wz310, wz4110, wz4111, new_primPlusNat0(wz123, Succ(Zero)), new_primPlusNat0(wz123, Succ(Zero)))
new_foldr10(wz310, Float(Pos(wz41000), wz4101), wz411, wz124, wz123) → new_foldr9(wz310, wz411, wz123)
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
The set Q consists of the following terms:
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr9(wz310, :(wz4110, wz4111), wz123) → new_foldr10(wz310, wz4110, wz4111, new_primPlusNat0(wz123, Succ(Zero)), new_primPlusNat0(wz123, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
- new_foldr10(wz310, Float(Neg(wz41000), wz4101), wz411, wz124, wz123) → new_foldr9(wz310, wz411, wz123)
The graph contains the following edges 1 >= 1, 3 >= 2, 5 >= 3
- new_foldr10(wz310, Float(Pos(wz41000), wz4101), wz411, wz124, wz123) → new_foldr9(wz310, wz411, wz123)
The graph contains the following edges 1 >= 1, 3 >= 2, 5 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldr11(wz82, wz800, :(wz8310, wz8311), wz175) → new_foldr12(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz175, Succ(Zero)), new_primPlusNat0(wz175, Succ(Zero)))
new_foldr12(wz82, wz800, Float(Pos(wz83000), wz8301), :(wz8310, wz8311), wz176, wz175) → new_foldr12(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz175, Succ(Zero)), new_primPlusNat0(wz175, Succ(Zero)))
new_foldr12(wz82, wz800, Float(Neg(wz83000), wz8301), wz831, wz176, wz175) → new_foldr11(wz82, wz800, wz831, wz175)
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
The set Q consists of the following terms:
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr12(wz82, wz800, Float(Neg(wz83000), wz8301), wz831, wz176, wz175) → new_foldr11(wz82, wz800, wz831, wz175)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 6 >= 4
- new_foldr12(wz82, wz800, Float(Pos(wz83000), wz8301), :(wz8310, wz8311), wz176, wz175) → new_foldr12(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz175, Succ(Zero)), new_primPlusNat0(wz175, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4
- new_foldr11(wz82, wz800, :(wz8310, wz8311), wz175) → new_foldr12(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz175, Succ(Zero)), new_primPlusNat0(wz175, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
new_psPs6(wz173, Zero, wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs7(wz173, Zero, wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_foldr14(wz82, wz800, Float(Neg(wz83000), wz8301), wz831, wz174, wz173) → new_psPs7(wz173, new_primMulNat0(Succ(wz82), wz83000), wz800, wz8301, wz82, wz831)
new_psPs6(wz173, Succ(wz1880), wz800, Pos(wz83010), wz82, :(wz8310, wz8311)) → new_foldr14(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz173, Succ(Zero)), new_primPlusNat0(wz173, Succ(Zero)))
new_foldr13(wz82, wz800, :(wz8310, wz8311), wz173) → new_foldr14(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz173, Succ(Zero)), new_primPlusNat0(wz173, Succ(Zero)))
new_psPs7(wz173, Succ(wz1890), wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs6(wz173, Succ(wz1880), wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs7(wz173, Zero, wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_foldr14(wz82, wz800, Float(Pos(wz83000), wz8301), wz831, wz174, wz173) → new_psPs6(wz173, new_primMulNat0(Succ(wz82), wz83000), wz800, wz8301, wz82, wz831)
new_psPs6(wz173, Zero, wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs7(wz173, Succ(wz1890), wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_psPs6(wz173, Zero, wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs7(wz173, Zero, wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_foldr14(wz82, wz800, Float(Neg(wz83000), wz8301), wz831, wz174, wz173) → new_psPs7(wz173, new_primMulNat0(Succ(wz82), wz83000), wz800, wz8301, wz82, wz831)
new_psPs6(wz173, Succ(wz1880), wz800, Pos(wz83010), wz82, :(wz8310, wz8311)) → new_foldr14(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz173, Succ(Zero)), new_primPlusNat0(wz173, Succ(Zero)))
new_foldr13(wz82, wz800, :(wz8310, wz8311), wz173) → new_foldr14(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz173, Succ(Zero)), new_primPlusNat0(wz173, Succ(Zero)))
new_psPs7(wz173, Succ(wz1890), wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs6(wz173, Succ(wz1880), wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs7(wz173, Zero, wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_foldr14(wz82, wz800, Float(Pos(wz83000), wz8301), wz831, wz174, wz173) → new_psPs6(wz173, new_primMulNat0(Succ(wz82), wz83000), wz800, wz8301, wz82, wz831)
new_psPs6(wz173, Zero, wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
new_psPs7(wz173, Succ(wz1890), wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Succ(wz400000)) → Succ(wz400000)
new_primPlusNat0(Succ(wz5300), Succ(wz400000)) → Succ(Succ(new_primPlusNat0(wz5300, wz400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wz5300), Zero) → Succ(wz5300)
new_primMulNat0(Succ(wz3100), Zero) → Zero
new_primMulNat0(Succ(wz3100), Succ(wz40100)) → new_primPlusNat1(new_primMulNat0(wz3100, Succ(wz40100)), wz40100)
new_primMulNat0(Zero, Succ(wz40100)) → Zero
new_primPlusNat1(Zero, wz40000) → Succ(wz40000)
new_primPlusNat1(Succ(wz530), wz40000) → Succ(Succ(new_primPlusNat0(wz530, wz40000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primMulNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr13(wz82, wz800, :(wz8310, wz8311), wz173) → new_foldr14(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz173, Succ(Zero)), new_primPlusNat0(wz173, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4
- new_foldr14(wz82, wz800, Float(Pos(wz83000), wz8301), wz831, wz174, wz173) → new_psPs6(wz173, new_primMulNat0(Succ(wz82), wz83000), wz800, wz8301, wz82, wz831)
The graph contains the following edges 6 >= 1, 2 >= 3, 3 > 4, 1 >= 5, 4 >= 6
- new_foldr14(wz82, wz800, Float(Neg(wz83000), wz8301), wz831, wz174, wz173) → new_psPs7(wz173, new_primMulNat0(Succ(wz82), wz83000), wz800, wz8301, wz82, wz831)
The graph contains the following edges 6 >= 1, 2 >= 3, 3 > 4, 1 >= 5, 4 >= 6
- new_psPs6(wz173, Succ(wz1880), wz800, Pos(wz83010), wz82, :(wz8310, wz8311)) → new_foldr14(wz82, wz800, wz8310, wz8311, new_primPlusNat0(wz173, Succ(Zero)), new_primPlusNat0(wz173, Succ(Zero)))
The graph contains the following edges 5 >= 1, 3 >= 2, 6 > 3, 6 > 4
- new_psPs7(wz173, Zero, wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs7(wz173, Succ(wz1890), wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs7(wz173, Zero, wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs7(wz173, Succ(wz1890), wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs6(wz173, Zero, wz800, Pos(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs6(wz173, Succ(wz1880), wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs6(wz173, Zero, wz800, Neg(wz83010), wz82, wz831) → new_foldr13(wz82, wz800, wz831, wz173)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4